#import "@preview/frame-it:1.1.2": *
#import "@preview/equate:0.3.1": equate
#import "RoseL_Snippets.typ": *


#title[数理逻辑]
= 命题
数学语言脱胎于自然语言, 
是在辩论和说服中产生, 并得到规范的. 
#definition[命题 (proposition)][
  #term[命题]是一个陈述或一般疑问, 它 
  #forward[要么] 是 #forward[真的] , 
  #forward[要么] 是 #forward[假的] .
]
// 哦不，先声概念太多了。

#example[][#ul[陈胜]者, #ul[阳城]人也. ]
#example[][#ul[管仲]俭乎？]

为了书写的方便, 我们未经定义地引入了"真"等一系列概念. 
其实这个做法相当危险, 但是可以直接用字母 $p, q$ 或者 
$T$ 表示命题, 而绕过对命题定义的后半句的严格判断. 

#definition[真 (true)][
  #term[真]是一个@命题\对自身的#forward[蕴含]. 
  $ 真 := a -> a $
]

什么是真? 自圆其说就是真的. 
自圆其说就是由自己能推出自己. 
// 那什么是蕴含呢? 
// 这个命题是什么命题? 是任设的某个命题, 无论真假. 
// 所以说无论真假都可以自圆其说. 
// 那么什么是假呢? 并非真的就是假的. 
// 那么或呢? 非此即彼. 
// 是呢?
// 
#notation[蕴含 $->$ (conditional)][前件 (antecedent)][后件 (consequence)][
  #term[蕴含]是关于两个@命题\的#forward[谓词], 
  通常说成 "如果#term[前件], 那么#term[后件]", 
  记作 $ P_a -> P_c $
]
#notation[否定 $not$ (negation)][#text(fill: gray)[被否定]项 (#text(fill: gray)[negated] component)][
  #term[否定]是关于一个@命题\的#forward[谓词], 
  通常说成 "并非#term[项]", 
  记作 $ not P_c $
]
否定的更常见写法是在被否定的#forward[关系符]上打一斜线. 

#axiom[蕴含-否定系统的公理化方案][
  #place[
    #set par(spacing: 1em)
    #term[前提引入]

    #term[前提分配]
    
    #linebreak()

    #term[否定消除]

    #term[否定引入]
  ]
  $ 
    a &--> (b -> a) 
    #<antec_gen>\
    (c->(b->a)) &--> ((c->b)->(c->a))\
    ((c->b)->(c->a)) &-->  (c->(b->a))
    #<antec_alloc>\
    (not a -> not b) &--> (b -> a)
    #<neg_gen>\
    a &--> not (not a)
    #<neg_neg>\
  $
]<ax_imp_neg>
一个@命题\成立了, 就可以给这个@命题\加一个前提条件, 这个词也是 "前件" 的来源. 
蕴含式也可以给它加一个前提条件, 而这相当于给它的前件和后件分别加这个前提条件; 
反之, 如果一个蕴含式的前件和后件都是蕴含式而且有共同的前件, 那么这个共同的前件可以提取出来. 
充分使用@否定消除\公理, 可以很容易知道@否定消除\公理和@否定引入\公理是可逆的.
// 但它们的逆命题是因否定逻辑的对称性而成立的. 
但是@前提分配\式的逆命题依赖蕴含式的结构而成立, 故而其充分性和必要性是独立的.
// 因此必须把@前提分配\式写成#forward[等价]\式. 

自然语言的疑问句, 是从陈述句改造来的, 可以对句子的任何成分进行提问.
当然了, 这样会把这个句子成分变成不明确的, 所以问句不能表达命题. 
有问就有答. 答就是注入信息: 把所答的内容填入问句的疑问词中, 再按文法整理成完整的陈述句. 
这刚好符合数学语言自由生成@命题\的需求. 
#example[][孰美? 君美甚.]

#notation[谓词 (predicate)][参数 (parameter)][
  #term[谓词]是部分待定的语句. 
  定义@谓词\时, 给个名字, 
  设一组#term[参数], 写下一个含有@参数\的语句.
  // 虽然没有集合论, 但是也可以讨论论域！即使是文法上也有这样的要求. 

  使用@谓词\时, 在@谓词\后给个实际值, 
  即得@谓词\在实际值处的@命题. 
  把定义谓词时写下的语句, 
  所有@参数\各自全部替换为相应实际值, 
  就是这个命题的写法.
]<note_predicate>

自然语言的文法通常把语句划分为主语和谓语, 语句去掉主语后的一切成分都是谓语.
数学语言把主语和谓语的关系推广, 
选一个符号, 把语句中这个符号出现的地方统统挖去, 
剩下的就成了关于这个符号的@谓词.
只要给定一个实际值, 向语句中被挖去的地方统统填入这个实际值, 
就形成了一个新的@命题. 
这个填法又叫做向@谓词\中#term[代入]实际值. 

#example[][//所有的示例都是超时空的
  $ P(x) := (x in NN) $
  $ P(0) = (0 in NN) $
]

虽然问句不能表达@命题, 但是问句能十分健康地表达@谓词. 
反之, 如果直接加工陈述句, 全部替换有时不那么方便. 
比如直接问 "谁不是马克思主义者?" 比较简单, 
但原@命题\是汉语 "马克思不是马克思主义者"时, 把 "马克思" 替换成 "凯恩斯", 
只能得到 "凯恩斯不是凯恩斯主义者", 而不是 "凯恩斯不是马克思主义者". 
这是我们为了部分替换和多元替换的方便而采取的规范的写法. 

我们以公理化的方式引入以下两个谓词. 先介绍它们的写法. 


// 用自蕴含引入真命题后
这也就是说：
#definition[命题][
 Proposition is 
 a statement or problem 
 that must be solved or proved 
 to be true or not true. 
]